M:MsgA. M.X  Type 

latex

Definitions	MsgA, M.X, b, x  dom(f), IdDeq, a:A fp B(a), x. t(x), x:A. B(x), Id, t  T
Lemmas	Id wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, assert wf, msga wf